$\forall$${\it da}_{1}$,${\it da}_{2}$:fpf(Knd; $x$.Type).
\\[0ex]normal{-}da\{i:l\}(${\it da}_{1}$) $\Rightarrow$ normal{-}da\{i:l\}(${\it da}_{2}$) $\Rightarrow$ normal{-}da\{i:l\}(fpf{-}join(Kind{-}deq; ${\it da}_{1}$; ${\it da}_{2}$))